(declare-fun P1 (Int Int Int) Bool)
(declare-fun P2 (Int) Bool)
(declare-fun P3 (Int Int Int) Bool)
(declare-fun P4 (Int Int Int Int Int Int Int) Bool)
(declare-fun P5 (Int Int Int) Bool)
(assert (forall ((v1 Int) (v2 Int) (v3 Int)) (=> (and (P5 v3 v2 v1)) (P3 v3 v2 v1))))
(assert (forall ((v1 Int) (v2 Int) (v3 Int) (v4 Int) (v5 Int) (v6 Int) (v7 Int) (v8 Int)) (let ((a!1 (= (not (= 0 v7)) (and (not (= 0 v6)))))) (let ((a!2 (and a!1 (= (not (= 0 v6)) (>= v5 0)) (= v5 (+ v4)) (= v4 v3) (not (not (= 0 v7))) (P5 v3 v2 v1)))) (=> a!2 (P2 v8))))))
(assert (forall ((v1 Int) (v2 Int) (v3 Int)) (let ((a!1 (and (not (not (= 0 v1))) (P5 v3 v2 v1)))) (=> a!1 (P3 v3 v2 v1)))))
(assert (forall ((v1 Int) (v2 Int) (v3 Int) (v4 Int) (v5 Int) (v6 Int) (v7 Int)) (=> (and (P3 v2 v1 v7)) (P4 v6 v5 v4 v3 v2 v1 v7))))
(assert (forall ((v1 Int) (v2 Int) (v3 Int)) (=> (and (P3 v2 v1 v3)) (P1 v2 v1 v3))))
(assert (forall ((v1 Int) (v2 Int) (v3 Int) (v4 Int) (v5 Int)) (=> (and (= v5 v3) (= v4 1) (P1 v3 v2 v1)) (P5 v5 v3 v4))))
(assert (not (exists ((v1 Int)) (and (P2 v1)))))
(assert (forall ((v1 Int) (v2 Int) (v3 Int) (v4 Int) (v5 Int)) (let ((a!1 (= (not (= 0 v5)) (and (not (= 0 v4)))))) (let ((a!2 (and a!1 (= (not (= 0 v4)) (>= v1 0)) (not (= 0 v5))))) (=> a!2 (P1 v1 v3 v2))))))
(check-sat)
